Nuprl Lemma : nil_before
11,40
postcript
pdf
T
:Type,
x
,
y
:
T
. l_before(
x
;
y
; [];
T
)
False
latex
Definitions
True
,
P
Q
,
P
Q
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
prop{i:l}
,
t
T
Lemmas
false
wf
,
sublist
wf
,
iff
wf
origin
T:Type, x,y:T. l_before(x; y; []; T) 
False T:Type, x,y:T. l_before(x; y; []; T) False Q Q
Q Qx:A. B(x)
T